Inference at * 1 2 1 2 1 1 2 
Iof proof for Lemma fast-fib:



1. n : 
2. 0 < n
3. a, b:.
3. {m:| 
3. {k:.
3. {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib((n - 1)+k))} 
4. a : 
5. b : 
6. b1:.
6. {m:| 
6. {k:.
6. {(a+b = fib(k))
6. { ((k  0)  (b1 = 0))
6. { ((0 < k)  (b1 = fib(k - 1)))
6. { (m = fib((n - 1)+k))} 
7. m : 
8. k:.
8. (a+b = fib(k))  ((k  0)  (a = 0))  ((0 < k)  (a = fib(k - 1)))  (m = fib((n - 1)+k))
9. k : 
10. a = fib(k)
11. (k  0)  (b = 0)
12. (0 < k)  (b = fib(k - 1))
13. (k = 0)
  a+b = fib(k+1) 

latex

 by (RecUnfold `fib` 0) 
CollapseTHEN (((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0)))

CollapseTHEN (Auto')) 

latex

C1: 

C1: 14. (k+1 = 0)
C1: 15. (k+1 = 1)
C1:   a+b = fib((k+1) - 1)+fib((k+1) - 2)
C.

Definitions	Unit, P  Q, P  Q, T, p q, left + right, P  Q, , p  q, True, Type, x:A  B(x), b, A, b, (i = j), , s = t, , n+m, x:AB(x), t  T, #$n, P & Q, P  Q, x:A. B(x), , {x:A| B(x)} , fib(n)
Lemmas	eqtt to assert, assert of bor, or functionality wrt iff, eqff to assert, squash wf, true wf, bnot thru bor, assert of band, and functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bor wf, bool wf, band wf, bnot wf, not wf, assert wf, eq int wf